COMMENT ⊗   VALID 00003 PAGES
C REC  PAGE   DESCRIPTION
C00001 00001
C00002 00002	[Comments added later are in brackets].
C00016 00003	linenames: 
C00018 ENDMK
C⊗;
[Comments added later are in brackets].
the proof FLAT:

(DECL (FLAT) |GROUND⊗GROUND→GROUND| CONSTANT)

(AXIOM |∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))|)
2. ∀X U.FLAT(X,U)=IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))
   deps: NIL

(COMMENTL LNAME DEFINFO)

(DECL (FLATTEN) |GROUND→GROUND| CONSTANT)

(AXIOM
 |∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR X)|)
5. ∀X.FLATTEN(X)=IF ATOM X THEN LIST(X) ELSE FLATTEN(CAR X)*FLATTEN(CDR X)
   deps: NIL

(COMMENTL LNAME DEFINFO)

[After defining flat and flatten as above, we shall want to prove
∀x u. flat(x,u) = flatten x * u.

This doesn't take many steps, but this file includes many partial rewritings
in order to illustrate how rewriting works.

[First we prove that flat(x,u) is a list.  This takes but one step with
a rather complicated rewriting mode.  Some details later].
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO**SORTINFO))*NIL*([1#2#1#2]($DEFINFO**SORTINFO))*
  *SIMPINFO*NIL*([1](DER))*NIL| SORTINFO)
7. ∀X U.LISTP FLAT(X,U)
   deps: NIL

[Flatten is a bit simpler to prove to be a list].
(∀E PHI |λX.LISTP FLATTEN(X)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL**SIMPINFO*NIL))*NIL*
  ([1#1#2](&DEFINFO*NIL**SIMPINFO*NIL))*([1#1](IMP(LISTAPPEND)*DER))*NIL|
 SORTINFO)
8. ∀X.LISTP FLATTEN(X)
   deps: NIL

(LINENAME LISTPFLATTEN *)


(COMMENTL LNAME LISTPFLATTEN)

Now starts the main proof.  Notice that the result is an implication
in which the premiss is a valid formula.  EKL could prove this
formula and hence do the whole problem in one rewrite if it cculd
use the premiss of the formula to rewrite the conclusion.  Soon it
will be able to do this.
(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL*
  ([1#1#2](&DEFINFO**SIMPINFO*NIL))| LISTPFLATTEN SORTINFO)
10. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X,FLAT(Y,U))=FLATTEN(X)*FLATTEN(Y)*U))⊃
     (∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

[As it stand we have to prove the premiss of 18 in several steps.  We
begin by assuming the premiss of this premiss].
(ASSUME |(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)|)
11. (∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)
    deps: (11)

This is the result we want.  The remaining steps are putting on
quantifiers and discharging the assumption and a simple modus
ponens.
(TRW |FLAT(X,FLAT(Y,U))| |*11| LISTPFLATTEN SORTINFO)
12. FLAT(X,FLAT(Y,U))=FLATTEN(X)*(FLATTEN(Y)*U)
    deps: (11)

(∀I (U) 12)
13. ∀U.FLAT(X,FLAT(Y,U))=FLATTEN(X)*(FLATTEN(Y)*U)
    deps: (11)

Here we discharge the premiss.
(CI (11) 13 |NIL|)
14. (∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
     (∀U.FLAT(X,FLAT(Y,U))=FLATTEN(X)*FLATTEN(Y)*U)
    deps: NIL

(∀I (X Y) 14)
15. ∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
          (∀U.FLAT(X,FLAT(Y,U))=FLATTEN(X)*FLATTEN(Y)*U)
    deps: NIL

This step is just a modus ponens in the rather pompous guise necessitated
by the fact that EKL now works entirely by rewriting.  Perhaps some concession
to old-fashioned methods is required, or perhaps I just didn't do it right.
(TRW |∀X U.FLAT(X,U)=FLATTEN(X)*U| |IMP(10,15)*TAUT|)
16. ∀X U.FLAT(X,U)=FLATTEN(X)*U
    deps: NIL

In the following steps, we are starting the proof from the beginning
again gradually enlarging the rewrite rule.
We work on whe atom case first and then on the compound case.  Note
that much of this can be standardized and will work for many similar
problems.  This suggest making it into a macro.
(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION |NIL| LISTPFLATTEN
 SORTINFO)
17. (∀X.ATOM X⊃(∀U.FLAT(X,U)=FLATTEN(X)*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*$SIMPINFO*NIL))| LISTPFLATTEN SORTINFO)
18. (∀X.ATOM X⊃(∀U.X~U=X~NNIL*U))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*$SIMPINFO*NIL*$DEFINFO*NIL))| LISTPFLATTEN SORTINFO)
19. (∀X.IF NULL X~NNIL THEN ATOM X⊃(∀U.X~U=U)
         ELSE ATOM X⊃(∀U.X~U=CAR (X~NNIL)~(CDR (X~NNIL)*U)))∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*$SIMPINFO*NIL*$DEFINFO**SIMPINFO*NIL))| LISTPFLATTEN
 SORTINFO)
20. (∀X.TRUE)∧
    (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*$SIMPINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL| LISTPFLATTEN
 SORTINFO)
21. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL| LISTPFLATTEN SORTINFO)
22. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.FLAT(X~Y,U)=FLATTEN(X~Y)*U))⊃(∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

(∀E PHI |λX.∀U.FLAT(X,U)=FLATTEN(X)*U| SEXPINDUCTION
 |NIL*([1#1#1](&DEFINFO*NIL*$DEFINFO**SIMPINFO*NIL))*NIL*
  ([1#1#2](&DEFINFO**SIMPINFO))| LISTPFLATTEN SORTINFO)
23. (∀X Y.(∀U.FLAT(X,U)=FLATTEN(X)*U)∧(∀U.FLAT(Y,U)=FLATTEN(Y)*U)⊃
           (∀U.IF FALSE THEN (X~Y)~U ELSE FLAT(X,FLAT(Y,U))=
                IF FALSE THEN (X~Y)~NNIL ELSE FLATTEN(X)*FLATTEN(Y)*U))⊃
     (∀X U.FLAT(X,U)=FLATTEN(X)*U)
    deps: NIL

The initial proof  of listp flat(x,u) seemed a bit obscure, so we start
again trying to make it parallel to the immediately preceding proof.  We
haven't been entirely successful.
(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO**SORTINFO))| SORTINFO)
24. (∀X.ATOM X⊃(∀U.LISTP IF ATOM X THEN X~U ELSE FLAT(CAR X,FLAT(CDR X,U))))∧
    (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP FLAT(X~Y,U)))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO**SORTINFO*NIL))| SORTINFO)
25. (∀X.ATOM X⊃(∀U.LISTP X~U))∧
    (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP FLAT(X~Y,U)))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL**SORTINFO*NIL))| SORTINFO)
26. (∀X.TRUE)∧
    (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP FLAT(X~Y,U)))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL**SORTINFO*NIL))*NIL| SORTINFO)
27. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP FLAT(X~Y,U)))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL**SORTINFO*NIL))*NIL*
  ([1#1#2]($DEFINFO*NIL*SORTINFO*NIL))| SORTINFO)
28. (∀X Y.(∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃
           IF ATOM X~Y THEN ∀U.LISTP (X~Y)~U
            ELSE ∀U.LISTP FLAT(CAR (X~Y),FLAT(CDR (X~Y),U)))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL**SORTINFO*NIL))*NIL*
  ([1#1#2]($DEFINFO*NIL*SORTINFO*NIL))*NIL| SORTINFO)
29. (∀X Y.IF ATOM X~Y
           THEN (∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP (X~Y)~U)
           ELSE (∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃
                 (∀U.LISTP FLAT(CAR (X~Y),FLAT(CDR (X~Y),U))))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL

(∀E PHI |λX.∀U.LISTP FLAT(X,U)| SEXPINDUCTION
 |NIL*([1#1#1]($DEFINFO*NIL**SORTINFO*NIL))*NIL*
  ([1#1#2]($DEFINFO*NIL*SORTINFO*NIL))*SORTINFO*NIL| SORTINFO)
30. (∀X Y.IF ATOM X~Y
           THEN (∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃(∀U.LISTP (X~Y)~U)
           ELSE (∀U.LISTP FLAT(X,U))∧(∀U.LISTP FLAT(Y,U))⊃
                 (∀U.LISTP FLAT(CAR (X~Y),FLAT(CDR (X~Y),U))))⊃
     (∀X U.LISTP FLAT(X,U))
    deps: NIL


linenames: 
LISTPFLATTEN has line range: (FLAT#8)
SORTINFO has line range: (LISPAX#12 LISPAX#14 LISPAX#19 LISPAX#38 LISPAX#42
                          LISPAX#46 LISPAX#51 LISPAX#67)
SIMPINFO has line range: (LISPAX#14 LISPAX#17 LISPAX#21 LISPAX#23 LISPAX#25
                          LISPAX#27 LISPAX#29 LISPAX#31 LISPAX#40 LISPAX#44
                          LISPAX#48 LISPAX#55 LISPAX#57)
CONSFACTS has line range: (LISPAX#21 LISPAX#23 LISPAX#29 LISPAX#31)
LISTINDUCTION has line range: (LISPAX#33)
SEXPINDUCTION has line range: (LISPAX#35)
LISTAPPEND has line range: (LISPAX#51)
DEFINFO has line range: (LISPAX#53 LISPAX#61 LISPAX#64 LISPAX#69 LISPAX#75
                         FLAT#2 FLAT#5)
APPENDFACTS has line range: (LISPAX#55 LISPAX#57)
REVERSEAPPEND has line range: (LISPAX#71)